*****∧I INDUCTION;

1 ∀U.((NULL U∨(CDR U*NILL)=CDR U)⊃(U*NILL)=U)⊃∀U.(U*NILL)=U  

*****∀E APPEND U,NILL;

2 (U*NILL)=IF NULL U THEN NILL ELSE CONS(CAR U,CDR U*NILL)  

*****;

3 (U*NILL)=IF NULL U THEN NILL ELSE CONS(CAR U,CDR U*NILL)≡IF NULL U THEN (U*NILL)=NILL ELSE (U*NILL)=CONS(CAR U%
,CDR U*NILL)  

*****TAUT (NULL U⊃(U*NILL)=NILL)∧(¬NULL U⊃(U*NILL)=CONS(CAR U,CDR U*NILL)) ↑↑:↑;

4 (NULL U⊃(U*NILL)=NILL)∧(¬NULL U⊃(U*NILL)=CONS(CAR U,CDR U*NILL))  

*****∀E NULL U;

5 NULL U≡U=NILL  

*****∀E CONS3 U;

6 ¬NULL U⊃CONS(CAR U,CDR U)=U  

*****TAUTEQ NULL U⊃(U*NILL)=U ↑↑↑:↑↑;

7 NULL U⊃(U*NILL)=U  

*****ASSUME (CDR U*NILL)=CDR U;

8 (CDR U*NILL)=CDR U  (8)

*****SUBST ↑ IN ↑↑↑;

9 ¬NULL U⊃CONS(CAR U,CDR U*NILL)=U  (8)

*****⊃I ↑↑⊃↑;

10 (CDR U*NILL)=CDR U⊃(¬NULL U⊃CONS(CAR U,CDR U*NILL)=U)  

*****TAUTEQ (¬NULL U∧(CDR U*NILL)=CDR U)⊃(U*NILL)=U 4,↑;

11 (¬NULL U∧(CDR U*NILL)=CDR U)⊃(U*NILL)=U  

*****TAUTEQ (NULL U∨(CDR U*NILL)=CDR U)⊃(U*NILL)=U 7,↑;

12 (NULL U∨(CDR U*NILL)=CDR U)⊃(U*NILL)=U  

*****∀I ↑ U;

13 ∀U.((NULL U∨(CDR U*NILL)=CDR U)⊃(U*NILL)=U)  

*****⊃E ↑,1;

14 ∀U.(U*NILL)=U